Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by Hansson and Jonsson. PCTL is a useful logic for stating soft deadline properties, e.g. "after a request for a service, there is at least a 98% probability that the service will be carried out within 2 seconds". Akin CTL suitability for model-checking PCTL extension is widely used as a property specification language for probabilistic model checkers.
One of the possible syntax of PCTL is defined as follows:
Therein, is comparison operator and is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure is a quadruple , where
A path from a state is an infinite sequence of states . The n-th state of the path is denoted as and the prefix of of length is denoted as .
A probability measure of the set of path with the common prefix of length is equal to the product of transitions probabilitites along the prefix of the path:
For the probability measure is equal to .
Satisfaction relations , are inductively defined as follows: